\section{Related Work}
\label{sec:related}

In her paper ``Extended Static Checking for Haskell''\cite{danaesch} Dana Xu provides very different method for proving properties of Haskell programs. Properties, referred to as contracts, are expressed within a refinement type for the function\cite{hinze06typedcontracts}. She details a sound and complete projection of these typed contracts into the functional program itself, whereby any execution path that violates the contract is replaced with the symbol \li{BAD}. One can then check that these paths are unreachable in order to verify the property. 

Another method of verifying function programs is through the use of supercompilation\cite{bolingbroke10supercompilation} to prove operational equivalence. Supercompilation is broadly the process of reducing a functional term to an equivalent simpler one. One could use this to prove a property such as \li{leq x (add x y)} \li{= True} by supercompiling \li{leq x (add x y)} which does not contain \li{False}. This method has similarities to Dana Xu's approach, in that we reduce a term to one which syntactically cannot violate a property.

Lots of work has been done for the verification of properties in object-oriented languages through the use of SMT solvers. One example is Spec\#{}, a superset of C\#{}, which uses the Microsoft's Z3\cite{z3} SMT solver. Proofs of recursive functions can be done with pre and post conditions and showing the latter implies the former, akin to specifying an inductive hypothesis and step. However these conditions are often not derivable and have to be specified by the programmer, which removes a degree of automation from the tool.